/* Simple Train-Gate system
	OPEN LOOP BEHAVIOUR:
	Simplified version in which MACHINE controls sL directly
	ENV:
	Trains move one way on a railway line that 
	intersects with a road.
	There is a traffic light that causes trains 
	to stop as they approach a level-crossing.
	The gate must be down when the trains cross, 
	and up otherwise.
	REQ-1: [](trainOn -> gateDown)
	CHALLENGE: Describe SPEC so that ENV && SPEC ==> REQ
*/
#define trainAway sT == away
#define trainNear sT == near
#define trainOn sT == on
#define gateUp sG == up
#define gateDown sG == down
#define lightRed sL == red
#define lightGreen sL == green
/* The following should hold but does not
	[](trainOn -> gateDown)
*/

/* state of Train*/
mtype = {away, near, on};
mtype sT = away;

/* state of Gate*/
mtype = {up, down};
mtype sG = up;

/* state of Light*/
mtype = {green, red};
mtype sL = red;

/* signal Gate to go up or down */
bool uPulse = false; bool dPulse = false;

/* ENVIRONMENT = TRAIN || GATE
   Simplified view of Light to control Train
*/

/*
   in: dPulse, uPulse
   out: sG
*/
proctype GATE()
{
       do
       ::  d_step {(uPulse && sG == down)  -> sG = up};
       ::  d_step {(dPulse && sG == up)   -> sG = down};
       od
}

/*
   in: sL
   out: sT
*/
proctype TRAIN()
{
       do
       :: d_step {(sT == away) -> sT = near};
			/* ENV assumption train drivers obey lights */
       :: d_step {(sT == near && sL == green) -> sT = on};
       :: d_step {(sT == on) -> sT = away};
       od
}

/* SPECIFICATION of machine under construction
	in: sT, SG 
	out: uPulse, dPulse, sL 
*/
proctype MACHINE()
/* Simplified version in which MACHINE controls sL directly */
{
	do
	:: uPulse = true;
	:: uPulse = false;
	:: dPulse = true;
	:: dPulse = false;
	:: sL = red;
	:: sL = green;
	od
}

init
{	
	d_step{sT = away; sG = up; sL = red; 
	uPulse = false; dPulse = false};
	atomic{run TRAIN(); run GATE(); run MACHINE()}
}
